Aspects of Incompleteness: Chapter 1 読書録2
$ \mathrm{PR},$ \land,\lor,有界量化で閉じていて,↓を満たすような論理式の集合を$ \Sigma_n, \Pi_nという.
1. $ \Sigma_n \cup \Pi_n \sube \Sigma_{n+1} \cup \Pi_{n+1}
2. $ \xiが$ \Sigma_n / \Pi_nのとき$ \Pi_n /\Sigma_n
3. $ \xi_0が$ \Sigma_n / \Pi_n,$ \xi_1が$ \Pi_n/\Sigma_nのとき,$ \xi_0 \to \xi_1は$ \Pi_n/\Sigma_nとする.
4. $ \xiが$ \Sigma_n/\Pi_nで,$ \delta_\mathrm{f}(\vec{x},y)がFact2を満たすような論理式だとする.
$ \exists z \lbrack \delta_\mathrm{f}(\vec{x},z) \land \xi \rbrackは$ \forall z \lbrack \delta_\mathrm{f}(\vec{x},z) \to \xi \rbrackは$ \Sigma_n/\Pi_nである.
memoここ定義が変な気がする.
5. $ \Sigma_nは存在量化で閉じているものとする.
6. $ \Pi_nは全称量化で閉じているものとする.
ただし$ \Sigma_0 = \Pi_0 = \mathrm{PR}とする.
memoよっておそらく$ \mathrm{PR}を$ \Delta_0と呼んでも多分問題ないハズ
$ \mathrm{B}_n論理式とは$ \Sigma_nのBoolean combinationsの集合とする.
Boolean combinationsって何?
$ \Phiは$ \Sigma_n,\Pi_n,\mathrm{B}_nのいずれかの論理式のクラスの集合とする.
理論$ Tに対して$ \Phi^T = \{ \xi \mid \eta \in \Phi : T \vdash \xi \leftrightarrow \eta \}と定める.
すなわち$ T上ではクラス$ \Phiの何らかの論理式と同値
論理式が$ \Delta_n^Tであるとは,$ \Pi_nかつ$ \Sigma_n^Tであること,もしくは$ \Sigma_nかつ$ \Pi^T_nとする.
$ \Delta_n = \Delta_n^\mathbf{PA}とする.
以降
$ \Gammaは$ \Sigma_{n+1}あるいは$ \Pi_{n+1}(すなわち$ \Sigma_1,\Pi_1以上)のどちらか
$ \Gamma^+は$ \Sigma_nあるいは$ \Pi_nのどちらか
とする.
論理式のクラス$ \Gammaの双対$ \Gamma^dは$ \Sigma_n^d = \Pi_n,$ \Pi_n^d = \Sigma_nと約束する.
d. $ \Sigma_n論理式および$ \Pi_n論理式のGödel数の集合も原始再帰的である.
a. $ \Sigma_{n+1}文$ \sigmaに対して,次の(自由変項$ xをただ1つ持つ)$ \Pi_n論理式$ \pi(x)を実行的に見出すことが出来る.
$ \mathbf{PA} \vdash \sigma \leftrightarrow \exists x \lbrack \pi(x) \rbrack
remark$ \exists x \lbrack \pi(x) \rbrackは$ \Sigma_{n+1}文である.
b. $ \Pi_{n+1}文$ \piに対して,次の(自由変項$ xをただ1つ持つ)$ \Sigma_n論理式$ \sigma(x)を実行的に見出すことが出来る.
$ \mathbf{PA} \vdash \pi \leftrightarrow \exists x \lbrack \sigma(x) \rbrack
remark$ \exists x \lbrack \sigma(x) \rbrackは$ \Pi_{n+1}文である
b. Fact 3.aの論理式,すなわち再帰的関数を定義する論理式は$ \Sigma_1として定義できる.
1. 再帰的関係$ \rm Rに対して$ \Sigma_1論理式が存在し,それゆえ$ \bf Q上で$ \Pi_1論理式によって表現される. 2. 再帰的可算関係$ \rm Rに対して$ \Sigma_1論理式が存在し,それゆえ$ \bf Q上で$ \Pi_1論理式によって弱表現される. proof
Cor 1より従うらしい.
Def
理論$ Tが$ \Gamma健全とは,任意の$ \Gamma文に対して$ Tで証明できる$ \iff真であることを指す.
$ Tを$ \Sigma_1健全とする.任意の再帰的可算集合$ \rm Xに対し,$ \rm Xを$ T上で表現する$ \Sigma_1論理式が存在する.
proof
再帰的可算集合$ \rm Xに対して,原始再帰的な関係$ \rm R(k,m)が存在し$ \rm X = \{ k \mid \exists m.R(k,m) \}である.
このことに注意すればCor2.2より
関係$ \rm R(k,m)が原始再帰的$ \iff$ \bf Q上で$ \rm Rを表現する$ \Delta_0論理式$ \rho(k,m)が存在する.
$ \chi(k) \equiv \exists m \lbrack \rho(k,m) \rbrackとする.
$ \chiは定義より$ \Sigma_1論理式であり,$ \Sigma_1健全性より$ \chiは$ T上で証明可能となるので$ \chiは$ \mathrm Xを弱表現する.
関数$ \rm f(\vec{k})が$ T上で可証再帰的(provably recursive)であるとは $ \Sigma_1論理式$ \delta_\mathrm{f}(\vec{x},y)が存在し
1. $ T \vdash \delta_\mathrm{f}(\vec{k},y) \leftrightarrow y = \overline{\rm f(\vec{k})}
2. $ T \vdash \delta_\mathrm{f}(\vec{k},y) \land \delta_\mathrm{f}(\vec{k},z) \to y = z
3. $ T \vdash \exists y \lbrack \delta_\mathrm{f}(\vec{x},y) \rbrack
remark
Fact 2は,原始再帰的関数は$ \bf PA上で可証再帰的であるということを述べている.
Remark
可証再帰的な関数$ \rm fについてもやっぱりそれに対応した関数記号と公理を$ Tに追加した新しい理論$ T'は$ Tの保存的拡大となる.
Memo
$ \alpha(x), \beta(x)は$ \Sigma_{n+1}論理式とし,$ \mathrm{f}(\vec{\mathrm{k}})は可証再帰的とする. 次の論理式は必ずしも$ \Sigma_{n+1}ではないが,$ \Sigma^T_{n+1}である.
1. $ \exists x \lbrack \alpha(x) \land \forall y \leq f(\vec{x}) \lbrack \beta(y) \rbrack \rbrack
なぜか?$ T上でこれと同値であるから
$ \exists x,z \lbrack \alpha(x) \land \delta_\mathrm{f}(\vec{x},z) \land \forall y \leq z \lbrack \beta(y) \rbrack \rbrack
同様にこれも$ \Pi^T_{n+1}である.
2. $ \forall x \lbrack \alpha(x) \land \exists y \leq f(\vec{x}) \lbrack \beta(y) \rbrack \rbrack
1,2を含むと$ \Sigma_{n+1},\Pi_{n+1}は非再帰的になってしまう.
SnO2WMaN.iconと書かれているがこの議論は意味不明だ
Memo
Fact4bで登場した,自由変数への数項の代入操作を表す原始再帰的関数$ \mathrm{subst}_1(\mathrm{k,m,n})を取ってくる.
$ \mathrm{subst_1}(\mathrm{k,m,n})は式$ \rm{n}が何らかの論理式のGödel数であったとき,その論理式に現れる自由変項$ v_\mathrm{k}を$ \mathrm{m}の数項$ mで置き換えて得られる論理式のGödel数を返す関数とする.
$ \mathrm{subst}(\mathrm{k}, \mathrm{m}, \ulcorner \xi(v_\mathrm{k}) \urcorner) = \xi(m)となる.
$ \mathrm{subst_2}(\mathrm{k_0,m_0,k_1,m_1,n}) := \mathrm{subst_1}(\mathrm{k_0},\mathrm{m_0},\mathrm{subst_1}(\mathrm{k_1},\mathrm{m_1},\mathrm{n}))と定義する.
Fact 2より,対応して$ \mathrm{Subst_1}(x,y,z,u)と$ \mathrm{Subst_1}(x_0,y_0,x_1,y_1,z,u)となる次の論理式が存在する.
$ \mathbf{Q} \vdash \mathrm{Subst_1}(k,m, \overline{\ulcorner \xi(v_\mathrm{k}) \urcorner}, u) \leftrightarrow u = \overline{\ulcorner \xi(m) \urcorner}
$ \mathbf{Q} \vdash \mathrm{Subst_2}(k_0,m_0,k_1,m_1, \overline{\ulcorner \eta(v_\mathrm{k_0},v_\mathrm{k_1}) \urcorner}, u) \leftrightarrow u = \overline{\ulcorner \eta(m_0,m_1) \urcorner}
$ \xiに現れる自由変項が$ v_\mathrm{k}ただ一つであるとき,
$ v_\mathrm{k}に$ xを代入した結果の論理式を$ \xi(\dot{x})と書く.
すなわち$ \ulcorner \xi(\dot{x}) \urcorner = \mathrm{subst}(\mathrm{k},\mathrm{x},\ulcorner \xi \urcorner)となる.
$ \etaに現れる自由変項が$ v_\mathrm{k},v_\mathrm{m}の2つであるとき,
同様に$ v_\mathrm{k},v_\mathrm{m}に$ x,yを代入した結果の論理式を$ \xi(\dot{x},\dot{y})と書く.
2個以上の場合も同様にする.
Memo
論理式$ \sigma(z)に対して
$ \mathrm{Prf}_\sigma(x,y)を直感的に次を表している論理式だと考える.
1. ある$ vが存在して
$ (y)_v = x
$ u > vに対して$ (y)_u = 0
$ u \leq vに対して$ (y)_uは
$ \sigma(z)を充足する($ \sigma(z)が表現する理論のGödel数全体に一致する?)
$ v < uの何らか$ (y)_vから推論規則で導かれる
2. $ yは文$ xの理論$ \sigma(z)を充足する証明である
もし$ \sigma(z)が$ \Gamma^+($ \Sigma_n,\Pi_nで$ n \ge 0)の場合$ \mathrm{Prf}_\sigma(x,y)も$ \Gamma^+として取ることができる.
$ \mathrm{Pr}_\sigma(x) \equiv \exists y\mathrm{Prf}_\sigma(x,y)
$ \mathrm{Con}_\sigma \equiv \lnot \mathrm{Pr}_\sigma(\ulcorner \bot \urcorner)
$ \sigma(z)は無矛盾
$ \sigma(z)が$ \Sigma_{n+1}なら$ \mathrm{Pr}_\sigma(x)も$ \Sigma_{n+1}で$ \mathrm{Con}_\sigmaは$ \Pi_{n+1}
任意の$ \sigma(x)に対して↓と定める.
$ (\sigma | y)(x) \equiv \sigma(x) \land x \le y
$ (\sigma + y)(x) \equiv \sigma(x) \lor x = y
次の表記を曖昧に用いる.理論$ Sを$ \Delta_0論理式$ \sigmaで表現されるとする.
$ \mathrm{Prf}_S(x,y): $ \mathrm{Prf}_\sigma(x,y)
$ \mathrm{Prf}_{S | z}(x,y): $ \mathrm{Prf}_{\sigma|z}(x,y)
$ \mathrm{Prf}_{S+z}(x,y): $ \mathrm{Prf}_{\sigma+z}(x,y)
$ \mathrm{Pr}_{S}(x,y)や$ \mathrm{Con}_\sigmaも同様に定める.
もし
$ Sが空集合であるとき,$ \sigma(x) \equiv \lnot x = xとする
$ Sが有限個であるとき:$ S = \{ \varphi_0,\dots,\varphi_n \},$ \sigma(x) \equiv x = \varphi_0 \lor \cdots \lor x = \varphi_nと定める.
Fact 6.
$ \vdash \forall \lbrack x(\sigma) \to \sigma'(x) \rbrack \to \forall y \lbrack \mathrm{Pr}_\sigma(y) \to \mathrm{Pr}_{\sigma'}(y) \rbrack
直ちに,$ \vdash \forall \lbrack x(\sigma) \to \sigma'(x) \rbrack \to ( \mathrm{Con}_{\sigma'} \to \mathrm{Con}_\sigma )
$ \mathrm{Pr}_\sigmaの定義を考えれば対偶を取って明らか
Fact 7.
$ \sigma(x)が$ T上で理論$ Sを弱表現しているとする a. $ pが$ \varphiの$ Sでの証明のとき,$ T \vdash \mathrm{Prf}_\sigma(\varphi,p)
b. $ S \vdash \varphiのとき,$ T \vdash \mathrm{Pr}_\sigma(\varphi)
c. $ Tが$ \bf PA拡大とする.自由変項$ x_0,\dots,x_nの論理式$ \alpha(x_0,\dots,x_{n-1})に対して
$ S \vdash \alpha(x_0,\dots,x_{n-1})のとき$ T \vdash \mathrm{Pr}_\sigma(\alpha(\dot{x_0},\dots,\dot{x_{n-1}}))
d. もし$ \sigma(x)が$ T上で$ Sを表現するなら,$ pが$ \varphiの$ Sでの証明でないとき$ T \vdash \lnot\mathrm{Prf}_\sigma(\varphi,p)
Fact 8
$ \sigma(x)は適当な論理式とする.
1. $ \mathbf{PA} \vdash \mathrm{Pr}_\sigma(x) \land \mathrm{Pr}_\sigma(x \to y) \to \mathrm{Pr}_\sigma(y)
2. $ \mathbf{PA} \vdash \mathrm{Pr}_{\sigma+y}(z) \leftrightarrow \mathrm{Pr}_\sigma(y \to z)
3. $ \mathbf{PA} \vdash \mathrm{Pr}_\sigma(x) \to \exists y\mathrm{Pr}_{\sigma|y}(x)
もし$ xが$ \sigma(x)上で証明できるなら,何らか理論を絞ることができる
Cor 5
$ \sigma(x)は適当な論理式とする.
1. $ \mathbf{PA} \vdash \mathrm{Pr}_\sigma(\beta(\dot{x})) \to \mathrm{Pr}_\sigma(\exists x \beta(x))
2. $ \mathbf{PA} \vdash \mathrm{Pr}_\sigma(\forall x \beta(x)) \to \mathrm{Pr}_\sigma(\beta(\dot{x}))
3. $ \mathbf{PA} \vdash \mathrm{Pr}_\sigma(x) \land \mathrm{Pr}_\sigma(\lnot x) \to \lnot \mathrm{Con}_\sigma
proof:Fact 8.1より
4. $ \mathbf{PA} \vdash \mathrm{Pr}_\sigma(\lnot x) \leftrightarrow \lnot \mathrm{Con}_{\sigma+x}及び$ \mathbf{PA} \vdash \mathrm{Pr}_\sigma(x) \leftrightarrow \lnot \mathrm{Con}_{\sigma+\lnot x}
proof
Fact 8.2より
$ \mathbf{PA} \vdash \mathrm{Pr}_\sigma(x \to \bot) \to \mathrm{Pr}_{\sigma+x}(\bot)
$ \mathbf{PA} \vdash \mathrm{Pr}_\sigma(\lnot x \to \bot) \to \mathrm{Pr}_{\sigma+\lnot x}(\bot)
$ Tが$ \bf PA拡張であって$ T上で$ \sigma(x)が$ Sを弱表現しているとする
5. $ S \vdash \gamma(x) \to \delta(x)ならば$ T \vdash \mathrm{Pr}_\sigma(\gamma(\bar{x})) \to \mathrm{Pr}_\sigma(\delta(\bar{x}))
6. $ S \vdash \varphi \to \psiならば$ T \vdash \mathrm{Pr}_\sigma(\varphi) \to \mathrm{Pr}_\sigma(\psi)
Remark
$ \bf Qは$ \bf PA上で真な$ \Sigma_1を全て証明できる
すなわち$ \bf Qは$ \bf PAの証明能力上で$ \Sigma_1完全である.
$ \varphi,\delta(\vec{x})は$ \Sigma_1とする.
a. $ \varphiが真なら$ \mathbf{Q} \vdash \varphi
b. $ \mathbf{PA} \vdash \delta(\vec{x}) \to \mathrm{Pr}_\mathbf{Q}(\delta(\vec{\dot{x}}))
特に$ \mathbf{PA} \vdash \varphi \to \mathrm{Pr}_\mathbf{Q}(\varphi)
c. $ \delta(\vec{x})が$ \Delta_0なら,原始再帰的関数$ fが存在して$ \mathbf{PA} \vdash \delta(\vec{x}) \to \mathrm{Prf}_\mathbf{Q}(\delta(\vec{\dot{x}}),f(\vec{x}))
Remark
Fact 9.a.より$ \psiが$ \Pi_1で$ T + \psiが無矛盾なら,$ \psiは真.
SnO2WMaN.icon?
Cor 6.
$ \sigma(x)は$ \bf PA上で$ \bf Qの拡大理論を弱表現するとする.
a. $ \varphiが$ \Sigma_1文であるとき,$ \mathbf{PA} \vdash \varphi \to \mathrm{Pr}_\sigma(\varphi)
b. $ \sigma(x)が$ \Sigma_1で$ \tau(x)が$ \bf PA上で$ T($ \bf Q拡大)を弱表現するとする.
$ \mathbf{PA} \vdash \mathrm{Pr}_\sigma(\varphi) \to \mathrm{Pr}_\tau(\mathrm{Pr}_\sigma(\varphi))
特に$ \mathbf{PA} \vdash \mathrm{Pr}_\sigma(\varphi) \to \mathrm{Pr}_\mathbf{Q}(\mathrm{Pr}_\sigma(\varphi))
以下はBernays-Löbの導出可能性条件という.
BL1: $ T \vdash \varphi \implies \mathbf{PA} \vdash \mathrm{Pr}_T(\varphi)
BL2: $ \mathbf{PA} \vdash \mathrm{Pr}_T(\varphi) \land \mathrm{Pr}_T(\varphi \to \psi) \to \mathrm{Pr}_T(\psi)
BL3: $ \mathbf{PA} \vdash \mathrm{Pr}_T(\varphi) \to \mathrm{Pr}_T(\mathrm{Pr}_T(\psi))